Technique: Programming with Modalities
Modal logic revolves around two logical operators, whose meaning is "it is necessary that X" and "it is possible that X", respectively. The principles governing these operators turn out to be useful for reasoning about other concepts as well, like knowledge (in epistemic logic) or the progress of time (in linear temporal logic).
In computing, we can interpret logical operators as type constructors and their proof rules as syntactical constructs in a programming language (see also Technique: Programs are Proofs). This view on modalities has a number of applications, from showing the absence of side effects to tracking resource usage and modelling event-driven programming.